Inference at * 1 
Iof proof for Lemma before-hd:



1. T : Type
2. L : T List
3. 0 < ||L||
4. no_repeats(T;L)
5. x : T
6. x before hd(L)  L
7. x, y:T. x before y  L  ((x = y))
  False 

latex

 by ((((FHyp (-1) [-2]) 
CollapseTHENA (Auto))) 
CollapseTHEN (((InstLemma `hd-before` [T;L;x])

CollapseTHENA (((Auto) 
CollapseTHEN (((FLemma `l_before_member2` [-3]) 
CollapseTHEN (Auto
C)))))))) 

latex

C1: 

C1: 8. (x = hd(L))
C1: 9. hd(L) before x  L
C1:   False
C.

Definitions	A, x before y  l, no_repeats(T;l), a < b, type List, Type, ||as||, x:A. B(x), P  Q, x:AB(x), (x  l)
Lemmas	hd-before, l member wf, l before member2